#include "SeqSolver.h"
#include "hsl/utility/Assert.h"
#include "hsl/utility/Logger.h"

/// LruVariableContainer: Maintains a sorted list of 
/// variables. Pops the Lru variable from the front.

LruVariableContainer::LruVariableContainer(int numVariables)
{   
    for(int i = 0; i < numVariables; i++) {
        initVariable(i + 1);
    }
}

bool LruVariableContainer::isEmpty() const
{ return varToQMap.empty(); }

void LruVariableContainer::initVariable(Variable v)
{
    lruQ_.push_back(LruStruct(0, v));
    LruQ_::iterator i = --lruQ_.end();
    varToQMap.insert(std::make_pair(v, i));
}

Variable LruVariableContainer::getLruVariable() const 
{ return lruQ_.begin()->second; }

void LruVariableContainer::updateVariableUsed(int iteration, Variable v)
{
    VarToQMap::iterator i = varToQMap.find(v); 
    assert(i != varToQMap.end() && "variable not found");
    LruQ_::iterator ii = i->second;
    LruStruct s = *ii;
    /// move the used variable to the back of the queue
    lruQ_.erase(ii);
    lruQ_.push_back(LruStruct(iteration, v));  
    LruQ_::iterator newI = --lruQ_.end();
    varToQMap.insert(std::make_pair(v, newI));
}

bool UnsatisfiedClauseContainer::empty() const {
    return unsatisfied_.empty();
}

void UnsatisfiedClauseContainer::initializeUnsatisfiedClauses(const Solution& solution)
{
    solution_ = &solution;
    const Problem& problem = solution_->getProblem(); 
    for(Problem::ClauseConstIterator i = problem.getClauseBegin(); i != problem.getClauseEnd(); ++i) {
        Clause *c = *i;
        if(!solution_->isSatisfied(*c)) { unsatisfied_.insert(c); }
    }
}

void UnsatisfiedClauseContainer::updateUnsatisfiedClauses(Variable changed)
{
    const Problem& problem = solution_->getProblem(); 
    Problem::VarToClauseMapIteratorPair clausesRange = problem.getClausesContaining(changed); 
    for(Problem::VarToClauseMapIterator i = clausesRange.first; i != clausesRange.second; ++i) {
        Clause *c = i->second;
        if(!solution_->isSatisfied(*c)) { unsatisfied_.insert(c); }
        else { unsatisfied_.erase(c); }
    }
}

UnsatisfiedClauseContainer::ConstIterator UnsatisfiedClauseContainer::begin() const
{ return unsatisfied_.begin(); }

UnsatisfiedClauseContainer::ConstIterator UnsatisfiedClauseContainer::end() const
{ return unsatisfied_.end(); }

int UnsatisfiedClauseContainer::size() const
{ return unsatisfied_.size(); }

SATSeqSolver::SATSeqSolver(int maxIterCount)
: iterCount_(0), maxIterCount_(maxIterCount)
{
}

void SATSeqSolver::initializeProblem(const Problem& problem)
{
    HSL_LOG_DEBUG("Initialized with problem [" << problem << "]\n"); 
    problem_ = &problem;
    currSol_ = SolutionUPtr(new Solution(*problem_)); 
    unsatisfied_.initializeUnsatisfiedClauses(*currSol_); 
    lru_ = std::unique_ptr<LruVariableContainer>(new LruVariableContainer(problem_->getNumVariables()));
}

int SATSeqSolver::getCurrentSolutionCost() const {
    return unsatisfied_.size();
}

bool SATSeqSolver::succeeded() const {
    return unsatisfied_.empty();
}

bool SATSeqSolver::done() const {
    return (iterCount_ >= maxIterCount_) || succeeded(); 
}

bool SATSeqSolver::intensifyMove() {
    std::vector<VariableGoodness> vs = findImprovingIntensifyingMoves();
    if(vs.empty()) {
        // no improving move found
        return false;
    } else {
        Variable v = selectVariableToFlip(vs);    
        HSL_LOG_DEBUG("Intensify: flip variable [" << v << "]\n"); 
        flipVariable(v);
    }
    return true;
}

void SATSeqSolver::diversifyMove()
{
    HSL_MSG_ASSERT(!lru_->isEmpty(), "LRU list cannot be empty"); 
    Variable v = lru_->getLruVariable();
    HSL_LOG_DEBUG("Diversify: flip variable [" << v << "]\n"); 
    flipVariable(v); 
}

void SATSeqSolver::flipVariable(Variable v)
{
    currSol_->flipVariable(v);  
    lru_->updateVariableUsed(iterCount_, v); 
    unsatisfied_.updateUnsatisfiedClauses(v);
    if(getCurrentSolutionCost() < bestSolCost_) {
        bestSol_ = SolutionUPtr(new Solution(*currSol_));  
        bestSolCost_ = getCurrentSolutionCost();
    }
}

std::vector<SATSeqSolver::VariableGoodness> SATSeqSolver::findImprovingIntensifyingMoves() const {
    std::vector<VariableGoodness> g;
    for(UnsatisfiedClauseContainer::ConstIterator i = unsatisfied_.begin(); i != unsatisfied_.end(); ++i) {
        std::set<Variable> var = currSol_->computeUnsatisfiedVariables(**i); 
        std::for_each(var.begin(), var.end(), [&](Variable v) { 
            VariableGoodness vg;
            vg.v = v;
            vg.goodnessValue = 1;
            g.push_back(vg); 
        });
    }
    return g;
}

Variable SATSeqSolver::selectVariableToFlip(std::vector<SATSeqSolver::VariableGoodness>& options) const {
    return (options.begin() + std::rand() % options.size())->v; 
}

void SATSeqSolver::solve() {
    while(!done()) {
        std::unique_ptr<Solution> next;
        while(!done()) {
            bool improving = intensifyMove();
            if(!improving) break;
        }
        if(!done()) {
            diversifyMove();
        }
    }
    if(succeeded()) HSL_LOG_DEBUG("Solution found." << *currSol_ << "\n");
}